M:MsgA, l:IdLnk, tg:Id. M.dout2(l;tg)  M.dout(l,tg) 

latex

Definitions	IdLnk, t  T, Id, x:A. B(x), rcv(l,tg), KindDeq, Knd, x. t(x), f(x)?z, M.dout(l,tg), MsgA, M.dout2(l;tg)
Lemmas	msga wf, subtype rel self, fpf-cap wf, Knd wf, Kind-deq wf, rcv wf, Id wf, IdLnk wf